Example 4.7.15 in [Borralleras - PhD'03]

Summary: Ex4_7_15_Bor03

• CS-TRS format
• OBJ format
• Negative results:
  1. CSRPO
  2. Polynomials
• Positive results:
  1. CSMSPO
  2. Lucas' transformation (DP + Polynomials @ MuTerm)
  3. Zantema's transformation (DP + Polynomials @ MuTerm)
  4. Ferreira and Ribeiro's transformation (DP + Polynomials @ MuTerm)
  5. Giesl and Middeldorp's transformation (CiME)
  6. CSDP

CS-TRS Ex4_7_15_Bor03 (file Ex4_7_15_Bor03.csr)

Functions:  f 0 cons s p

Constructors:  0 cons s

Variables: 

Arities: 

ar(f) = 1
ar(0) = 0
ar(cons) = 2
ar(s) = 1
ar(p) = 1

Replacement map: 

µ(f)={1}
µ(0)={}
µ(cons)={1}
µ(s)={1}
µ(p)={1}

Rules: (file Ex4_7_15_Bor03)   

f(0) -> cons(0,f(s(0)))
f(s(0)) -> f(p(s(0)))
p(s(0)) -> 0

The CS-TRS in OBJ format (file Ex4_7_15_Bor03.obj):

obj Ex4_7_15_Bor03 is
  sort S .
  op f : S -> S .
  op 0 : -> S .
  op cons : S S -> S [strat (1 0)] .
  op s : S -> S .
  op p : S -> S .
  eq f(0) = cons(0,f(s(0))) .
  eq f(s(0)) = f(p(s(0))) .
  eq p(s(0)) = 0 .
endo

Negative results

1. The TRS Ex4_7_15_Bor03 is not simply µ-terminating [GL02b, Section 3]:

       f(s(0)) -> f(p(s(0)))
          ->_Embµ(F) f(s(0))
          -> ...
       

   Therefore, by [GL02b, Theorem 9] R cannot be proved mu-terminating by using CSRPO (see also [Bor03, Example 4.7.15]) or a polynomial interpretation.

Positive results

1. The µ-termination of Ex4_7_15_Bor03 is proved in [Bor03, Example 4.7.15] by using CSMSPO together with the following:
   • marking map:

     	   m(cons,2)=m(_cons,2)={f}
     	   m(from,1)={s}
     	   

   • >=_Q is defined as the lexicographic combination of a precedence >_F and an interpretation >=_I, where

     	   f >_F cons, s, _f, p
     	   

     and >=_I is defined by the combination of the interpretation generated by the pairs

     (cons(x,y),cons)

     and

     (p(x),0)

     and the indentity for the rest of symbols with RPO with the precedence >=_P given by

     	 f >P cons
     	 

2. The µ-termination of Ex4_7_15_Bor03 can also be proved by using Lucas' transformation. The TRS Ex4_7_15_Bor03_L:

        f(0) -> cons(0)
        f(s(0)) -> f(p(s(0)))
        p(s(0)) -> 0
        

   is terminating (use MuTerm).
3. The µ-termination of Ex4_7_15_Bor03 can also be proved by using Zantema's transformation. The TRS Ex4_7_15_Bor03_Z:

        f(0) -> cons(0,n__f(s(0)))
        f(s(0)) -> f(p(s(0)))
        p(s(0)) -> 0
        f(X) -> n__f(X)
        activate(n__f(X)) -> f(X)
        activate(X) -> X
        

   is terminating (use MuTerm).
4. The µ-termination of Ex4_7_15_Bor03 can also be proved by using Ferreira and Ribeiro's transformation. The TRS Ex4_7_15_Bor03_FR:

        f(0) -> cons(0,n__f(n__s(n__0)))
        f(s(0)) -> f(p(s(0)))
        p(s(0)) -> 0
        f(X) -> n__f(X)
        s(X) -> n__s(X)
        0 -> n__0
        activate(n__f(X)) -> f(activate(X))
        activate(n__s(X)) -> s(activate(X))
        activate(n__0) -> 0
        activate(X) -> X
        

   is terminating (use MuTerm).
5. The µ-termination of Ex4_7_15_Bor03 can also be proved by using Giesl and Middeldorp's transformation. The TRS Ex4_7_15_Bor03_GM:

       a__f(0) -> cons(0,f(s(0)))
       a__f(s(0)) -> a__f(a__p(s(0)))
       a__p(s(0)) -> 0
       mark(f(X)) -> a__f(mark(X))
       mark(p(X)) -> a__p(mark(X))
       mark(0) -> 0
       mark(cons(X1,X2)) -> cons(mark(X1),X2)
       mark(s(X)) -> s(mark(X))
       a__f(X) -> f(X)
       a__p(X) -> p(X)
       

   is terminating (use CiME).
6. The µ-termination of Ex4_7_15_Bor03 can also be proved by using CSDP (computed by MuTerm).